FDL - Step of Proof: fseg

Step of Proof: fseg_length

11,40

Inference at *
Iof proof for Lemma fseg length:

T:Type, l1, l2:(T List). fseg(T;l1;l2)

(||l1||

||l2||)

by ((((((((((Unfold `fseg` 0)

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n

C),(first_nat 3:n)) (first_tok :t) inil_term)))

)

CollapseTHEN (ExRepD))

)

CollapseTHEN (

CHypSubst (-1) 0))

)

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n

C)) (first_tok :t) inil_term)))

)

CollapseTHEN (((RWO "length_append" 0)

CollapseTHEN (

C(Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term)))

))

Definitions fseg(T;L1;L2), x:A. B(x), P Q, P & Q, x:A B(x), T, P Q, P Q, True, , i j , A B, n+m, , as @ bs, type List, Type, ||as||, x:A. B(x), x:AB(x), t T, s = t

Lemmas iff wf, rev implies wf, le wf, squash wf, true wf, length append, non neg length, length wf1

Definitions	fseg(T;L1;L2), x:A. B(x), P Q, P & Q, x:A B(x), T, P Q, P Q, True, , i j , A B, n+m, , as @ bs, type List, Type, \|\|as\|\|, x:A. B(x), x:AB(x), t T, s = t
Lemmas	iff wf, rev implies wf, le wf, squash wf, true wf, length append, non neg length, length wf1